#ifndef FORMULA_H
#define FORMULA_H

#include <string>
#include <vector>
using namespace std;

// forward declarations.
class Expression;
class BooleanExpression;
class Substitution;

/*
    Class: Formula
    Represents a formula.
*/
class Formula
{
    /* Section: public */
    public:
        /*
            Constructor: Default constructor.
            Initializes the object.
        */
        Formula(Expression * expression = NULL, vector<Substitution *> * substitutions = NULL);

        /*
            Constructor: Copy constructor.
            Initializes the object as copy from other Formula object.

            Parameters:
                other - Formula object to copy from.
        */
        Formula(const Formula & other);

        /*
            Destructor: Default destructor.
            Destroy the object.
        */
        virtual ~Formula();

        /*
            Method: setExpression
            Sets the expression of the formula.

            Parameters:
                expression  -   Expression to set.
        */
        void setExpression(Expression * expression);

        /*
            Method: addSubstitution
            Adds a substitution to the formula.

            Parameters:
                attribute   -   Attribute name to be substutited.
                expression  -   Expression thats substituted the attribute given.
        */
        void addSubstitution(const string & attribute, Expression * expression);

        /*
            Method: setSubstitutions
            Sets the substitutions of a formula.

            Parameters:
                substitutions
        */
        void setSubstitutions(vector<Substitution *> * substitutions);

        /*
            Method: getExpression
            Returns:
                The expression of the formula.
        */
        Expression * getExpression();

        /*
            Method: getSubstitutions
            Returns:
                A mapping with the substitutions in the formula.
        */
        vector<Substitution *> * getSubstitutions();

        /*
            Method: toString
            Returns:
                A string representation of a formula.
        */
        string toString();

        /*
            Method: clone
            Returns a clone of this object.
        */
        Formula * clone();

    /* Section: private*/
    private:
        /*
            Variable: expression.
            Type: BooleanExpression
            Expression of the formula.
        */
        Expression * expression;

        /*
            Variable: mapping
            Type: map of string to Expression objects.
            Implements the list of substitutions.
        */
        vector<Substitution *> * substitutions;
};

#endif // FORMULA_H
